the_es:ES, l:IdLnk, e:E. haslnk(l;e)   

latex

Definitions	Unit, P  Q, P & Q, Prop, b, A, false, b, isrcv(e), , E, IdLnk, ES, haslnk(l;e), Dec(P), P  Q, p  q, a = b, lnk(e), x:A. B(x), P  Q, t  T
Lemmas	es-lnk wf, eq lnk wf, band wf, es-isrcv wf, decidable assert, event system wf, IdLnk wf, es-E wf, bfalse wf, assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert